/* File parser.mly */

/* The Header */
%{
open Syntax
%}

/* The Grammar */
%token <string> TokenStr
%token TokenColon
%token TokenIf
%token TokenFi
%token TokenTo
%token TokenGoto
%token TokenTrue
%token TokenFalse
%token TokenLBr
%token TokenRBr
%token TokenAnd
%token TokenOr
%token TokenNot
%token TokenSkip
%token TokenEof

/* lowest precedence */
%left TokenOr
%left TokenAnd
%nonassoc TokenNot
/* highest precedence */


%start main            /* the entry point */
%type <Syntax.nba> main

%%

main:
	states TokenEof                        { $1 }
;

states:
                                                                         { [] }
	/* ltl2ba syntax: skip is last command + true gate to accept_all state */
	| TokenStr TokenColon TokenSkip                                       { [($1, [(True, "accept_all")])] }
	| TokenStr TokenColon TokenStr TokenColon TokenIf translist TokenFi states { ($1,$6)::$8 }
  	| TokenStr TokenColon TokenIf translist TokenFi states                { ($1,$4)::$6 }
;

translist:
                                                                         { [] }
  	| TokenColon TokenColon TokenFalse                                   { [] }
	| TokenColon TokenColon gate TokenTo TokenGoto TokenStr translist    { ($3,$6)::$7 }
;

gate:
	TokenFalse                             { False }
    | TokenTrue                              { True }
	| TokenStr                             { Prop $1 }
	| TokenLBr gate TokenRBr               { $2 }
	| gate TokenAnd gate							{ And ($1, $3) }  /* shift-reduce conflict */
	| gate TokenOr gate							{ Or ($1, $3) }  /* shift-reduce conflict */
	| TokenNot gate	        					{ Not $2 }
;;
